COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notions of finite union and finite sum
C00003 00003	(proof sums)
C00006 00004	(proof sumfacts)
C00008 00005	PROOFS
C00009 00006	bound quantifier
C00011 00007	proof of properties of union and sum
C00015 00008	a fix needed
C00016 ENDMK
C⊗;
;the notions of finite union and finite sum
(wipe-out)
(get-proofs appl prf ekl sys)

(proof sums)

(decl allnum (type: |ground⊗@set→truthval|) (syntype: constant))
(decl somenum (type: |ground⊗@set→truthval|) (syntype: constant))
(decl (numseq f) (type:|ground→ground|))
(decl sum (type: |(@numseq)⊗(@n)→(@n)|) (syntype: constant))
(decl setseq (type: |@n→@set|))
(decl un (type: |(@setseq)⊗(@n)→(@set)|) (syntype: constant))

;axiom for allnum
(defax allnum |∀n a.allnum(0,a)∧(allnum(n',a)≡a(n)∧allnum(n,a))|)
(label allnumdef)

;axiom for somenum
(defax somenum |∀n a.¬somenum(0,a)∧(somenum(n',a)≡a(n)∨somenum(n,a))|)
(label somenumdef)

;axiom for sum
(defax sum |∀n numseq.sum(numseq,0)=0∧sum(numseq,n')=sum(numseq,n)+numseq(n)|)
(label sumdef)

;axiom for un
(defax un |∀n setseq.un(setseq,0)=emptyset∧un(setseq,n')=un(setseq,n)∪setseq(n)|)
(label undef)

(decl disj_pair (syntype: constant) (type: |(@set⊗@set)→truthval|))
(define disj_pair |∀a b.disj_pair(a,b)=emptyp(a∩b)|)
(label disjpair_def)

(decl disjoint (syntype: constant) (type: |((ground→@set)⊗ground)→truthval|))
(defax disjoint |∀n setseq.disjoint(setseq,0)∧
    disjoint(setseq,n')=(disjoint(setseq,n)∧disj_pair(un(setseq,n),setseq(n)))| )
(label disjointdef)
(proof sumfacts)

;properties of allnum and somenum

(axiom |∀a n.(∀m.m<n⊃a(m))≡allnum(n,a)|)
(label allnumfact)

(axiom |∀a n.(∃m.m<n∧a(m))≡somenum(n,a)|)
(label somenumfact)

;properties of un

(axiom |∀setseq n m.m<n⊃setseq(m)⊂un(setseq,n)|)
(label unionfact1)

(axiom |∀u n.n≤length u⊃(un(λm.mkset(nth(u,m)),n))=(λx.(∃k.k<n∧nth(u,k)=x))|)
(label mksetfact)

(axiom |∀u.un(λm.mkset(nth(u,m)),length u)=(λx.(mklset(u))(x))|)
(label mklset_un)

;exercise: unionfact2 
;∀setseq n m.n<m⊃un(setseq,n)⊂un(setseq,m)

;properties of sum

(axiom |∀numseq n.(∀m.m<n⊃natnum(numseq(m)))⊃natnum(sum(numseq,n))|)
(label sumsort)

(save-proofs sums)
;PROOFS
;bound quantifier
    (proof allnumprop)

    ;we can easily prove that `allnum' does its job

1.  (ue ((a.|λn.allnum(n,a)⊃(m<n⊃a(m))|)) proof_by_induction
	 ((use transitivity_of_order) (use successor1) (open allnum)
	   (use less_succ_lesseq normal mode: exact) (open lesseq)))
    ;∀N.ALLNUM(N,A)⊃(M<N⊃A(M))

2.  (ue ((a.|λn.(∀m.m<n⊃a(m))⊃allnum(n,a)|)) proof_by_induction (open allnum)
	  (use normal mode: always)
	  (use less_succ_lesseq mode: exact) (open lesseq)))
    ;∀N.(∀M.M<N⊃A(M))⊃ALLNUM(N,A)

3.  (derive |∀n.(∀m.m<n⊃a(m))≡allnum(n,a)| (* -2))

    ;similarly for `somenum':

4.  (ue ((a.|λn.somenum(n,a)⊃(∃m.m<n∧a(m))|)) proof_by_induction
	 ((use transitivity_of_order) (use successor1) (open somenum) (part 1 (der))
	   (use less_succ_lesseq normal mode: exact) (open lesseq)))
    ;∀N.SOMENUM(N,A)⊃(∃M.M<N∧A(M))

5.  (ue ((a.|λn.(∃m.m<n∧a(m))⊃somenum(n,a)|)) proof_by_induction (open somenum)
	  (use normal mode: always) (part 1(der))
	  (use less_succ_lesseq mode: exact) (open lesseq)))
    ;∀N.(∃M.M<N∧A(M))⊃SOMENUM(N,A)

6.  (derive |∀n.(∃m.m<n∧a(m))≡somenum(n,a)| (* -2))

;proof of properties of union and sum
    (wipe-out)
    (get-proofs sums prf ekl sys)
    (proof unionprop)

    ;a property of union

    ;unionfact1

1.  (ue (a |λn.m<n⊃(∀xv.(setseq(m))(xv)⊃(un(setseq,n))(xv))|)
        proof_by_induction   
        (open un union) (use less_succ_lesseq mode: always)
        (open lesseq) (use normal mode: always))
    ;∀N.M<N⊃(∀XV.(SETSEQ(M))(XV)⊃(UN(SETSEQ,N))(XV))

    ;namely:

2.  (trw |∀setseq n m.m<n⊃setseq(m)⊂un(setseq,n)| * (open inclusion))
    (label unionfact1)

    ;a property of sum

    ;sumsort

3.  (ue (a |λn.allnum(n,λm.natnum numseq(m))⊃natnum sum(numseq,n)|) 
        proof_by_induction (open allnum sum))
    ;∀N.ALLNUM(N,λM.NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))

4.  (rw * (use allnumfact mode: exact direction: reverse))
    ;∀N.(∀M.M<N⊃NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))

    ;mksetfact

5.  (ue (a |λn.n≤length u⊃
                    (un(λm.mkset(nth(u,m)),n))(x)≡somenum(n,λk.x=nth(u,k))|)
        proof_by_induction 
        (part 1(open un mkset nth somenum union emptyset) (der))
        (use succ_lesseq_lesseq mode: always))
    ;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡SOMENUM(N,λK.X=NTH(U,K))

6.  (rw * (use somenumfact 
           ue: ((a.|λk.x=nth(u,k)|)(n.n)) mode: exact direction: reverse))
    ;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡(∃M.M<N∧X=NTH(U,M))

7.  (assume |n≤length u|)

8.  (ue ((av.|un(λm.mkset nth(u,m),n)|)
         (bv.|λx.∃k.k<n∧nth(u,k)=x|)) set_extensionality 
         (open epsilon)(use * -2 mode: always))
    ;UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))

9.  (ci -2)
    ;N≤LENGTH U⊃UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))

    ;mklset_un                                            

10. (ue (n |length u|) mksetfact 
        (use mklset_fact mode: exact direction: reverse) (open lesseq))
    ;∀U.UN(λM.MKSET(NTH(U,M)),LENGTH U)=MKLSET(U)

    ;;;;;;;
    ;used here:

    ;labels: TRANS_LESSEQ 
    ;∀N M K.N≤M∧M≤K⊃N≤K

    ;labels: SET_EXTENSIONALITY 
    ;∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV

    ;LABELS: SOMENUMFACT 
    ;∀A N.(∃M.M<N∧A(M))≡SOMENUM(N,A)

    ;labels: MKLSET_FACT 
    ;∀U.MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))
    ;namely:
;a fix needed
;fixed

(define consnumber |consnumber(0)=nil∧consnumber(n')=n.consnumber(n)|
        inductive_definition)

(trw |∀n.natnum consnumber(n)|)
;∀N.NATNUM(CONSNUMBER(N))

(axiom |∀numseq n.allnum(n,λm.natnum(numseq(m)))⊃natnum(sum(numseq,n))|)